Day 3 - I'm Attending ICFP & SPLASH 2025!

# Hatra: Usability Barriers for Liquid Types

The first HATRA talk was a report on a user study on the usability of liquid types (LiquidHaskell) for both new¹ and experienced users. This was extremely well presented and very useful reference for me as I have never actually seen a user study report and have been planning to perform one on my research in collaboration with the Future of Programming Lab led by Cyrus at Michigan in the future.

The study itself concluded by identifying a few usability barriers for liquid (refinement) types evidenced by the qualitative and quantitative results gathered during the study on their 19 participants. The barriers identified were classified into three groups:

# HATRA: Imperative Syntax for Dependent Types

Another well presented talk with great slides (manually syntax highlighted!!!!). The concept was to make dependent types more accessible to the 'average programmer', that is, one who has not done any functional programming (like most the people at this conference). While the syntax looked pretty good and definitely seemed more readable for such a programmer, I'm not really sure what the use case is because it is a 'read-only' language in the sense that to write in this language still requires proofs to type check, but I have absolutely no idea how this could be presented to the average imperative programmer who has no knowledge of this and maybe not even the mathematical understanding to write or understand them. In fact, how would this such a programmer even read a program with a proof?? I suspect it would come across as completely foreign to them. It'll be interesting to see how these issues are addressed in the future (this talk was about still very early stage reaearch).

# HATRA: Decomposable Type Highlighting in Hazel

Finally, we get to my talk! It actually somehow went faster than in the practice I had this morning, and felt like it went reasonably well for a first talk.

Briefly, my work has developed a formal foundation and peiminary implementation for highlighting parts of an expression and it's surrounding context which contribute to the type of the expression.³ Importantly, you can decompose the highlighting to take only the subpart of a type which you want to explain/look at, making it an interactive tool. I'll be posting an extended summary/abstract of the work itself and a review of future directions on a separate later post.

I got a couple of good questions plus some very fruitful discussion afterwards during the break. One attendee actually hinted me towards using least upper bound for a part of the research which I had struggled to formalise back while doing my undergrad dissertation to make the highlighting include both if statement branches rather than just one; of course, this generally ends up in too much code being highlighted but is an interesting theoretical idea, corresponding to not highlighting all terms which are provably not involved in deriving the type of the expression.

I was also able to discuss how the ideas might extend to allow non-local type information to be incorporated into this method, by 'gluing together' multiple program slices into another valid program. The current implementation already does this to an extent with respect to bindings (and their type slices), but what I really want is a formal foundation for this which can also be applied to a type system including unification or constraints allowing non-local inference (which is where confusion arises most, and where the tool would be most useful). The biggest issue is these glued programs are no longer slices of the original program; maybe I need a relaxation of slicing that allows restricted and orincipled restructuring of the program. This is a difficult problem which i will be considering as part of my master's project.

My main hope at this workshop was to get ideas on how to improve my UI for this tool, and I had a good discussion with someone afterwards about how to effectively select parts of the type of a term to focus on. This is non-trivial as the selections need to either select a slice or sub-term of the type, we can't just arbitrarily select any characters in the string representation and even if we could we still need to translate this back into a type. Options considered were both flat representations, i.e. clicking the text directly but with restrictions or toggling vs some more sophisticated tree based interfaces which could allow more 'continuous' selection⁴, but this might be less efficient for an experienced user. I suspect represented types as trees could also help learners as it makes explicit the precedence rules.

Anyway, very fruitful discussion, though perhaps less discussion about the core UI mechanism and human aspects than I desired.

# ICFP: Functional Networking for Millions of Docker Desktops

Brilliant talk by my supervisor Anil on how docker for desktop was initially created, focusing on the use of OCaml for core parts of the HyperKit and Vpnkit. That is, docker had to run on a Linux kernel, so for Mac they needed to simulate this, which they did by working out how to exploit the hypervisor for this, and then also used Ocaml for the networking, which also required some sort of spoofing to make it look like the packets were coming from the Mac OS rather than a rogue Linux kernel (which would look like a virus).

It's a really amazing example of how Ocaml can be used for really low level programming, even before the advent of modern features like multicore Ocaml and OxCaml. Hopefully more people use Ocaml for low level projects now we have even more sophisticated features!!

# Hatra: Types as a Specification Language for Creativity

This was an interesting talk on the idea of splitting a typing system into a pair of soft rules and hard rules: those that should be followed and those which must be followed. The application was for music counterpoint where some rules are just guidelines and others are more strict (e.g. intervals of 2nd and 7ths are hard and must never be used while 5ths and octaves are soft). Then a scoring system, somewhat similar to effect systems,⁵ is used to score the violation of soft rules (scoring 'how well' it meets the type system).

This definitely seems like it can be extended into an interesting way to formalise the ideas of 'warnings' (yellow squiggles) in programming static checkers.

The talk was quite short so we had a lot of time for questions, most of which focused on the art aspect. One person noted that even these hard rules are intentionally broken by experienced composers, yet the type system categorically disallows this; I note that a system like Hazel could still be used that marked errors, but still treats it as a valid program, in this situations letting the music play even with errors. Though, at thus point the distinction between hard and soft rules is blurred.

I had two questions in particular about how the type system could accommodation dependent rules, like forbidding parallel fifths, or preferring contrary motion. Apparently Youyou has formalised this but we didn't have any time to talk about this as she left early. One way to encode this that I did suggest was using type level functions, like a form of System F. Of course, dependent types are the way to go to model complex rules, but I suspect simple rules like parallel 5ths can be represented directly with only types and if statements in a system F style type-level language.

# HATRA: Discussion

There was a discussion session put on which I thought was an interesting idea, hoping I could maybe get some more HCI related feedback on my work, or discuss other ideas. But, it ended up trying to be a session to come up with theories for HCI at a high level, not relating to much specifically. While I definitely had some good discussion about how people reason about programming (notional machines), I don't think it really got anywhere substantive...

# Thoughts

Happy to have my talk dine, and another good set of talks to attend today. We later went out for dinner with Cyrus and were able to discuss my future plans in more detail. Turned out that Roly (who I'd never met before) was also joining, and we had some great discussion where he really did seem to get the fundamentals of what I was talking about. Roly's work on slicing methods were a big inspiration for the initial directions that my work took back a year ago. I definitely recommend reading Functional Programs that Explain their Work for a great accessible paper of one particular slicing method.